$\forall$$i$:Id, ${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), ${\it snd}$:msg{-}spec(${\it ds}$; ${\it da}$).
\\[0ex]msg{-}spec{-}loc{-}decl(${\it snd}$; $i$; ${\it da}$) $\Rightarrow$ msg{-}spec{-}loc(${\it snd}$; $i$)